master-antecedent{i:l}(es;Cmd;Master;Config;Sys;m)
== (e:{e:E(Master)| cmseq?(Master(e))} . (m(e) < e))
== & (e1, e2:{e:E(Master)| cmseq?(Master(e))} . (m(e1) <loc m(e2))  (e1 < e2))
== & (e:{e:E(Master)| cmseq?(Master(e))} .
== & (let c = Config(m(e)) in
== & (let c(ccpred?(c))
== & (let & ccpred-id(c) = cmseq-to(Master(e))
== & (let & loc(m(e)) = cmseq-from(Master(e))
== & (let & ||cmd-history(m(e))|| = cmseq-num(Master(e))) 

latex

---

clarification:

master-antecedent{i:l}
master-antecedent(es; Cmd; Master; Config; Sys; m)
== (e:{e:es-E-interface(es;Master)| cmseq?(Master(e))} . es-causl(es; (m(e)); e))
== & (e1:{e:es-E-interface(es;Master)| cmseq?(Master(e))} ,
== & (e2:{e:es-E-interface(es;Master)| cmseq?(Master(e))} .
== & (es-locl(es; (m(e1)); (m(e2)))  es-causl(es; e1; e2))
== & (e:{e:es-E-interface(es;Master)| cmseq?(Master(e))} .
== & (let c = Config(m(e)) in
== & (let c(ccpred?(c))
== & (let & ccpred-id(c) = cmseq-to(Master(e))  Id
== & (let & es-loc(es; (m(e))) = cmseq-from(Master(e))  Id
== & (let & ||cmd-history{i:l}(es; Config; Cmd; Sys; (m(e)))|| = cmseq-num(Master(e))  ) 

latex

Definitions	P  Q, (e <loc e'), (e < e'), x:A. B(x), {x:A| B(x)} , E(X), cmseq?(x), let x = a in b(x), b, ccpred?(x), ccpred-id(x), cmseq-to(x), P & Q, Id, loc(e), cmseq-from(x), s = t, , ||as||, cmd-history(e), f(a), cmseq-num(x), X(e)
FDL editor aliases	master-antecedent